YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(s(X)) -> f(X)
  , g(cons(s(X), Y)) -> s(X)
  , g(cons(0(), Y)) -> g(Y)
  , h(cons(X, Y)) -> h(g(cons(X, Y))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { g(cons(0(), Y)) -> g(Y) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [f](x1) = [3] x1 + [1]         
                                          
           [s](x1) = [1] x1 + [0]         
                                          
           [g](x1) = [1] x1 + [0]         
                                          
    [cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                          
               [0] = [1]                  
                                          
           [h](x1) = [2] x1 + [1]         
  
  This order satisfies the following ordering constraints:
  
             [f(s(X))] =  [3] X + [1]        
                       >= [3] X + [1]        
                       =  [f(X)]             
                                             
    [g(cons(s(X), Y))] =  [1] X + [1] Y + [0]
                       >= [1] X + [0]        
                       =  [s(X)]             
                                             
     [g(cons(0(), Y))] =  [1] Y + [1]        
                       >  [1] Y + [0]        
                       =  [g(Y)]             
                                             
       [h(cons(X, Y))] =  [2] X + [2] Y + [1]
                       >= [2] X + [2] Y + [1]
                       =  [h(g(cons(X, Y)))] 
                                             

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(s(X)) -> f(X)
  , g(cons(s(X), Y)) -> s(X)
  , h(cons(X, Y)) -> h(g(cons(X, Y))) }
Weak Trs: { g(cons(0(), Y)) -> g(Y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { f(s(X)) -> f(X) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [f](x1) = [3] x1 + [3]         
                                          
           [s](x1) = [1] x1 + [1]         
                                          
           [g](x1) = [1] x1 + [0]         
                                          
    [cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                          
               [0] = [0]                  
                                          
           [h](x1) = [2] x1 + [1]         
  
  This order satisfies the following ordering constraints:
  
             [f(s(X))] =  [3] X + [6]        
                       >  [3] X + [3]        
                       =  [f(X)]             
                                             
    [g(cons(s(X), Y))] =  [1] X + [1] Y + [1]
                       >= [1] X + [1]        
                       =  [s(X)]             
                                             
     [g(cons(0(), Y))] =  [1] Y + [0]        
                       >= [1] Y + [0]        
                       =  [g(Y)]             
                                             
       [h(cons(X, Y))] =  [2] X + [2] Y + [1]
                       >= [2] X + [2] Y + [1]
                       =  [h(g(cons(X, Y)))] 
                                             

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { g(cons(s(X), Y)) -> s(X)
  , h(cons(X, Y)) -> h(g(cons(X, Y))) }
Weak Trs:
  { f(s(X)) -> f(X)
  , g(cons(0(), Y)) -> g(Y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

Trs: { g(cons(s(X), Y)) -> s(X) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [f](x1) = [3] x1 + [1]         
                                          
           [s](x1) = [1] x1 + [2]         
                                          
           [g](x1) = [1] x1 + [0]         
                                          
    [cons](x1, x2) = [1] x1 + [1] x2 + [2]
                                          
               [0] = [0]                  
                                          
           [h](x1) = [2] x1 + [1]         
  
  This order satisfies the following ordering constraints:
  
             [f(s(X))] =  [3] X + [7]        
                       >  [3] X + [1]        
                       =  [f(X)]             
                                             
    [g(cons(s(X), Y))] =  [1] X + [1] Y + [4]
                       >  [1] X + [2]        
                       =  [s(X)]             
                                             
     [g(cons(0(), Y))] =  [1] Y + [2]        
                       >  [1] Y + [0]        
                       =  [g(Y)]             
                                             
       [h(cons(X, Y))] =  [2] X + [2] Y + [5]
                       >= [2] X + [2] Y + [5]
                       =  [h(g(cons(X, Y)))] 
                                             

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs: { h(cons(X, Y)) -> h(g(cons(X, Y))) }
Weak Trs:
  { f(s(X)) -> f(X)
  , g(cons(s(X), Y)) -> s(X)
  , g(cons(0(), Y)) -> g(Y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.

Trs: { h(cons(X, Y)) -> h(g(cons(X, Y))) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA) and not(IDA(1)).
  
           [f](x1) = [3 0] x1 + [3]           
                     [3 0]      [3]           
                                              
           [s](x1) = [1 0] x1 + [0]           
                     [0 0]      [0]           
                                              
           [g](x1) = [1 0] x1 + [0]           
                     [0 0]      [0]           
                                              
    [cons](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                     [0 0]      [0 0]      [2]
                                              
               [0] = [0]                      
                     [0]                      
                                              
           [h](x1) = [1 2] x1 + [0]           
                     [0 0]      [1]           
  
  This order satisfies the following ordering constraints:
  
             [f(s(X))] =  [3 0] X + [3]          
                          [3 0]     [3]          
                       >= [3 0] X + [3]          
                          [3 0]     [3]          
                       =  [f(X)]                 
                                                 
    [g(cons(s(X), Y))] =  [1 0] X + [1 0] Y + [0]
                          [0 0]     [0 0]     [0]
                       >= [1 0] X + [0]          
                          [0 0]     [0]          
                       =  [s(X)]                 
                                                 
     [g(cons(0(), Y))] =  [1 0] Y + [0]          
                          [0 0]     [0]          
                       >= [1 0] Y + [0]          
                          [0 0]     [0]          
                       =  [g(Y)]                 
                                                 
       [h(cons(X, Y))] =  [1 0] X + [1 0] Y + [4]
                          [0 0]     [0 0]     [1]
                       >  [1 0] X + [1 0] Y + [0]
                          [0 0]     [0 0]     [1]
                       =  [h(g(cons(X, Y)))]     
                                                 

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { f(s(X)) -> f(X)
  , g(cons(s(X), Y)) -> s(X)
  , g(cons(0(), Y)) -> g(Y)
  , h(cons(X, Y)) -> h(g(cons(X, Y))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))